That's a very standard way of doing these things. We're

using deduction as an inference process. We could have used either tableau or

resolution and you can imagine that having efficient inference procedures is

is very important for agents because they want to be able to react quickly

or have a very good

world network.